(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 5))
(let ((e4 (* v1 e3)))
(let ((e5 (- v0 e4)))
(let ((e6 (* v0 v0)))
(let ((e7 (- v2)))
(let ((e8 (> e7 e5)))
(let ((e9 (> e6 e5)))
(let ((e10 (>= e5 e7)))
(let ((e11 (<= e6 e4)))
(let ((e12 (> e4 v2)))
(let ((e13 (distinct e7 e4)))
(let ((e14 (>= v2 e5)))
(let ((e15 (< v0 v2)))
(let ((e16 (= v2 v1)))
(let ((e17 (< e5 e4)))
(let ((e18 (>= e5 e4)))
(let ((e19 (>= v0 e4)))
(let ((e20 (<= v1 v1)))
(let ((e21 (distinct e4 e6)))
(let ((e22 (< v1 v0)))
(let ((e23 (< v1 e6)))
(let ((e24 (= e6 v2)))
(let ((e25 (> v0 v0)))
(let ((e26 (distinct e4 v0)))
(let ((e27 (>= e7 v2)))
(let ((e28 (xor e26 e8)))
(let ((e29 (ite e21 e27 e10)))
(let ((e30 (= e25 e20)))
(let ((e31 (=> e24 e23)))
(let ((e32 (and e17 e17)))
(let ((e33 (xor e30 e12)))
(let ((e34 (= e19 e33)))
(let ((e35 (or e16 e14)))
(let ((e36 (= e13 e22)))
(let ((e37 (xor e29 e36)))
(let ((e38 (= e34 e35)))
(let ((e39 (not e37)))
(let ((e40 (or e9 e9)))
(let ((e41 (and e40 e18)))
(let ((e42 (not e28)))
(let ((e43 (ite e38 e31 e31)))
(let ((e44 (ite e11 e42 e39)))
(let ((e45 (= e32 e32)))
(let ((e46 (= e44 e43)))
(let ((e47 (not e46)))
(let ((e48 (= e45 e47)))
(let ((e49 (ite e41 e48 e41)))
(let ((e50 (and e49 e15)))
e50
)))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
